(declare-fun k () Real)
(declare-fun a () Real)
(declare-fun c () Real)
(declare-fun b () Real)
(declare-fun l () Real)
(declare-fun e () Real)
(declare-fun d () Real)
(declare-fun m () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun n () Real)
(declare-fun f () Real)
(declare-fun j () Real)
(assert (not (exists ((i Real)) (=> (=> (<= i 0) (< i e)) (<= l m) (<= 0 h)))))
(assert (= k (* l n)))
(assert (= l (/ k n)))
(assert (= n (* k l) a (- e n)))
(assert (= e (/ a n)))
(assert (= n (/ a e) (/ n d)))
(assert (distinct c f))
(assert (= f (/ c m) 0))
(assert (= g (mod (to_int b) (to_int j)) (/ b g)))
(check-sat)
